Left Termination of the query pattern ack(b,b,f) w.r.t. the given Prolog program could successfully be proven:



↳ PROLOG
  ↳ PrologToPiTRSProof

ack3(00, N, s1(N)).
ack3(s1(M), 00, A) :- ack3(M, s1(00), A).
ack3(s1(M), s1(N), A) :- ack3(s1(M), N, A1), ack3(M, A1, A).


With regard to the inferred argument filtering the predicates were used in the following modes:
ack3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


ack_3_in_gga3(0_0, N, s_11(N)) -> ack_3_out_gga3(0_0, N, s_11(N))
ack_3_in_gga3(s_11(M), 0_0, A) -> if_ack_3_in_1_gga3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ack_3_in_gga3(s_11(M), s_11(N), A) -> if_ack_3_in_2_gga4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
if_ack_3_in_2_gga4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> if_ack_3_in_3_gga5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
if_ack_3_in_3_gga5(M, N, A, A1, ack_3_out_gga3(M, A1, A)) -> ack_3_out_gga3(s_11(M), s_11(N), A)
if_ack_3_in_1_gga3(M, A, ack_3_out_gga3(M, s_11(0_0), A)) -> ack_3_out_gga3(s_11(M), 0_0, A)

The argument filtering Pi contains the following mapping:
ack_3_in_gga3(x1, x2, x3)  =  ack_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ack_3_out_gga3(x1, x2, x3)  =  ack_3_out_gga1(x3)
if_ack_3_in_1_gga3(x1, x2, x3)  =  if_ack_3_in_1_gga1(x3)
if_ack_3_in_2_gga4(x1, x2, x3, x4)  =  if_ack_3_in_2_gga2(x1, x4)
if_ack_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ack_3_in_3_gga1(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

ack_3_in_gga3(0_0, N, s_11(N)) -> ack_3_out_gga3(0_0, N, s_11(N))
ack_3_in_gga3(s_11(M), 0_0, A) -> if_ack_3_in_1_gga3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ack_3_in_gga3(s_11(M), s_11(N), A) -> if_ack_3_in_2_gga4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
if_ack_3_in_2_gga4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> if_ack_3_in_3_gga5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
if_ack_3_in_3_gga5(M, N, A, A1, ack_3_out_gga3(M, A1, A)) -> ack_3_out_gga3(s_11(M), s_11(N), A)
if_ack_3_in_1_gga3(M, A, ack_3_out_gga3(M, s_11(0_0), A)) -> ack_3_out_gga3(s_11(M), 0_0, A)

The argument filtering Pi contains the following mapping:
ack_3_in_gga3(x1, x2, x3)  =  ack_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ack_3_out_gga3(x1, x2, x3)  =  ack_3_out_gga1(x3)
if_ack_3_in_1_gga3(x1, x2, x3)  =  if_ack_3_in_1_gga1(x3)
if_ack_3_in_2_gga4(x1, x2, x3, x4)  =  if_ack_3_in_2_gga2(x1, x4)
if_ack_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ack_3_in_3_gga1(x5)


Pi DP problem:
The TRS P consists of the following rules:

ACK_3_IN_GGA3(s_11(M), 0_0, A) -> IF_ACK_3_IN_1_GGA3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ACK_3_IN_GGA3(s_11(M), 0_0, A) -> ACK_3_IN_GGA3(M, s_11(0_0), A)
ACK_3_IN_GGA3(s_11(M), s_11(N), A) -> IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
ACK_3_IN_GGA3(s_11(M), s_11(N), A) -> ACK_3_IN_GGA3(s_11(M), N, A1)
IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> IF_ACK_3_IN_3_GGA5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> ACK_3_IN_GGA3(M, A1, A)

The TRS R consists of the following rules:

ack_3_in_gga3(0_0, N, s_11(N)) -> ack_3_out_gga3(0_0, N, s_11(N))
ack_3_in_gga3(s_11(M), 0_0, A) -> if_ack_3_in_1_gga3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ack_3_in_gga3(s_11(M), s_11(N), A) -> if_ack_3_in_2_gga4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
if_ack_3_in_2_gga4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> if_ack_3_in_3_gga5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
if_ack_3_in_3_gga5(M, N, A, A1, ack_3_out_gga3(M, A1, A)) -> ack_3_out_gga3(s_11(M), s_11(N), A)
if_ack_3_in_1_gga3(M, A, ack_3_out_gga3(M, s_11(0_0), A)) -> ack_3_out_gga3(s_11(M), 0_0, A)

The argument filtering Pi contains the following mapping:
ack_3_in_gga3(x1, x2, x3)  =  ack_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ack_3_out_gga3(x1, x2, x3)  =  ack_3_out_gga1(x3)
if_ack_3_in_1_gga3(x1, x2, x3)  =  if_ack_3_in_1_gga1(x3)
if_ack_3_in_2_gga4(x1, x2, x3, x4)  =  if_ack_3_in_2_gga2(x1, x4)
if_ack_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ack_3_in_3_gga1(x5)
IF_ACK_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ACK_3_IN_2_GGA2(x1, x4)
ACK_3_IN_GGA3(x1, x2, x3)  =  ACK_3_IN_GGA2(x1, x2)
IF_ACK_3_IN_1_GGA3(x1, x2, x3)  =  IF_ACK_3_IN_1_GGA1(x3)
IF_ACK_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_ACK_3_IN_3_GGA1(x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

ACK_3_IN_GGA3(s_11(M), 0_0, A) -> IF_ACK_3_IN_1_GGA3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ACK_3_IN_GGA3(s_11(M), 0_0, A) -> ACK_3_IN_GGA3(M, s_11(0_0), A)
ACK_3_IN_GGA3(s_11(M), s_11(N), A) -> IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
ACK_3_IN_GGA3(s_11(M), s_11(N), A) -> ACK_3_IN_GGA3(s_11(M), N, A1)
IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> IF_ACK_3_IN_3_GGA5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> ACK_3_IN_GGA3(M, A1, A)

The TRS R consists of the following rules:

ack_3_in_gga3(0_0, N, s_11(N)) -> ack_3_out_gga3(0_0, N, s_11(N))
ack_3_in_gga3(s_11(M), 0_0, A) -> if_ack_3_in_1_gga3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ack_3_in_gga3(s_11(M), s_11(N), A) -> if_ack_3_in_2_gga4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
if_ack_3_in_2_gga4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> if_ack_3_in_3_gga5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
if_ack_3_in_3_gga5(M, N, A, A1, ack_3_out_gga3(M, A1, A)) -> ack_3_out_gga3(s_11(M), s_11(N), A)
if_ack_3_in_1_gga3(M, A, ack_3_out_gga3(M, s_11(0_0), A)) -> ack_3_out_gga3(s_11(M), 0_0, A)

The argument filtering Pi contains the following mapping:
ack_3_in_gga3(x1, x2, x3)  =  ack_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ack_3_out_gga3(x1, x2, x3)  =  ack_3_out_gga1(x3)
if_ack_3_in_1_gga3(x1, x2, x3)  =  if_ack_3_in_1_gga1(x3)
if_ack_3_in_2_gga4(x1, x2, x3, x4)  =  if_ack_3_in_2_gga2(x1, x4)
if_ack_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ack_3_in_3_gga1(x5)
IF_ACK_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ACK_3_IN_2_GGA2(x1, x4)
ACK_3_IN_GGA3(x1, x2, x3)  =  ACK_3_IN_GGA2(x1, x2)
IF_ACK_3_IN_1_GGA3(x1, x2, x3)  =  IF_ACK_3_IN_1_GGA1(x3)
IF_ACK_3_IN_3_GGA5(x1, x2, x3, x4, x5)  =  IF_ACK_3_IN_3_GGA1(x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 2 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

ACK_3_IN_GGA3(s_11(M), s_11(N), A) -> IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
ACK_3_IN_GGA3(s_11(M), s_11(N), A) -> ACK_3_IN_GGA3(s_11(M), N, A1)
IF_ACK_3_IN_2_GGA4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> ACK_3_IN_GGA3(M, A1, A)
ACK_3_IN_GGA3(s_11(M), 0_0, A) -> ACK_3_IN_GGA3(M, s_11(0_0), A)

The TRS R consists of the following rules:

ack_3_in_gga3(0_0, N, s_11(N)) -> ack_3_out_gga3(0_0, N, s_11(N))
ack_3_in_gga3(s_11(M), 0_0, A) -> if_ack_3_in_1_gga3(M, A, ack_3_in_gga3(M, s_11(0_0), A))
ack_3_in_gga3(s_11(M), s_11(N), A) -> if_ack_3_in_2_gga4(M, N, A, ack_3_in_gga3(s_11(M), N, A1))
if_ack_3_in_2_gga4(M, N, A, ack_3_out_gga3(s_11(M), N, A1)) -> if_ack_3_in_3_gga5(M, N, A, A1, ack_3_in_gga3(M, A1, A))
if_ack_3_in_3_gga5(M, N, A, A1, ack_3_out_gga3(M, A1, A)) -> ack_3_out_gga3(s_11(M), s_11(N), A)
if_ack_3_in_1_gga3(M, A, ack_3_out_gga3(M, s_11(0_0), A)) -> ack_3_out_gga3(s_11(M), 0_0, A)

The argument filtering Pi contains the following mapping:
ack_3_in_gga3(x1, x2, x3)  =  ack_3_in_gga2(x1, x2)
0_0  =  0_0
s_11(x1)  =  s_11(x1)
ack_3_out_gga3(x1, x2, x3)  =  ack_3_out_gga1(x3)
if_ack_3_in_1_gga3(x1, x2, x3)  =  if_ack_3_in_1_gga1(x3)
if_ack_3_in_2_gga4(x1, x2, x3, x4)  =  if_ack_3_in_2_gga2(x1, x4)
if_ack_3_in_3_gga5(x1, x2, x3, x4, x5)  =  if_ack_3_in_3_gga1(x5)
IF_ACK_3_IN_2_GGA4(x1, x2, x3, x4)  =  IF_ACK_3_IN_2_GGA2(x1, x4)
ACK_3_IN_GGA3(x1, x2, x3)  =  ACK_3_IN_GGA2(x1, x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ PiDPToQDPProof
                ↳ QDP
                  ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

ACK_3_IN_GGA2(s_11(M), s_11(N)) -> IF_ACK_3_IN_2_GGA2(M, ack_3_in_gga2(s_11(M), N))
ACK_3_IN_GGA2(s_11(M), s_11(N)) -> ACK_3_IN_GGA2(s_11(M), N)
IF_ACK_3_IN_2_GGA2(M, ack_3_out_gga1(A1)) -> ACK_3_IN_GGA2(M, A1)
ACK_3_IN_GGA2(s_11(M), 0_0) -> ACK_3_IN_GGA2(M, s_11(0_0))

The TRS R consists of the following rules:

ack_3_in_gga2(0_0, N) -> ack_3_out_gga1(s_11(N))
ack_3_in_gga2(s_11(M), 0_0) -> if_ack_3_in_1_gga1(ack_3_in_gga2(M, s_11(0_0)))
ack_3_in_gga2(s_11(M), s_11(N)) -> if_ack_3_in_2_gga2(M, ack_3_in_gga2(s_11(M), N))
if_ack_3_in_2_gga2(M, ack_3_out_gga1(A1)) -> if_ack_3_in_3_gga1(ack_3_in_gga2(M, A1))
if_ack_3_in_3_gga1(ack_3_out_gga1(A)) -> ack_3_out_gga1(A)
if_ack_3_in_1_gga1(ack_3_out_gga1(A)) -> ack_3_out_gga1(A)

The set Q consists of the following terms:

ack_3_in_gga2(x0, x1)
if_ack_3_in_2_gga2(x0, x1)
if_ack_3_in_3_gga1(x0)
if_ack_3_in_1_gga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_ACK_3_IN_2_GGA2, ACK_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: